Nuprl Lemma : irrefl_trans_imp_sasym 13,42

T:Type, R:(TT). irrefl(T;R trans(T;R st_anti_sym(T;R
latex


Upgen algebra 1
Definitions of Statementtrans(T;E), irrefl(T;R), st_anti_sym(T;R)
Definitionst  T, P & Q, A, StAntiSym(T;x,y.R(x;y)), st_anti_sym(T;R), P  Q, , x:AB(x), Irrefl(T;x,y.E(x;y)), Trans(T;x,y.E(x;y)), trans(T;E), irrefl(T;R), False
Lemmasxxirrefl wf, xxtrans wf

origin